(0) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
m2(S(0), b, res, True) → False
m2(S(S(x)), b, res, True) → True
m2(0, b, res, True) → False
m3(S(0), b, res, t) → False
m3(S(S(x)), b, res, t) → True
m3(0, b, res, t) → False
l8(res, y, res', True, mtmp, t) → res
l5(x, y, res, tmp, mtmp, True) → 0
help1(S(0)) → False
help1(S(S(x))) → True
e4(a, b, res, False) → False
e4(a, b, res, True) → True
e2(a, b, res, False) → False
l15(x, y, res, tmp, False, t) → l16(x, y, gcd(y, 0), tmp, False, t)
l15(x, y, res, tmp, True, t) → l16(x, y, gcd(y, S(0)), tmp, True, t)
l13(x, y, res, tmp, False, t) → l16(x, y, gcd(0, y), tmp, False, t)
l13(x, y, res, tmp, True, t) → l16(x, y, gcd(S(0), y), tmp, True, t)
m4(S(x'), S(x), res, t) → m5(S(x'), S(x), monus(x', x), t)
m2(a, b, res, False) → m4(a, b, res, False)
l8(x, y, res, False, mtmp, t) → l10(x, y, res, False, mtmp, t)
l5(x, y, res, tmp, mtmp, False) → l7(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, False) → l3(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, True) → res
l11(x, y, res, tmp, mtmp, False) → l14(x, y, res, tmp, mtmp, False)
l11(x, y, res, tmp, mtmp, True) → l12(x, y, res, tmp, mtmp, True)
help1(0) → False
e2(a, b, res, True) → e3(a, b, res, True)
bool2Nat(False) → 0
bool2Nat(True) → S(0)
m1(a, x, res, t) → m2(a, x, res, False)
l9(res, y, res', tmp, mtmp, t) → res
l6(x, y, res, tmp, mtmp, t) → 0
l4(x', x, res, tmp, mtmp, t) → l5(x', x, res, tmp, mtmp, False)
l1(x, y, res, tmp, mtmp, t) → l2(x, y, res, tmp, mtmp, False)
e7(a, b, res, t) → False
e6(a, b, res, t) → False
e5(a, b, res, t) → True
monus(a, b) → m1(a, b, False, False)
m5(a, b, res, t) → res
l7(x, y, res, tmp, mtmp, t) → l8(x, y, res, equal0(x, y), mtmp, t)
l3(x, y, res, tmp, mtmp, t) → l4(x, y, 0, tmp, mtmp, t)
l16(x, y, res, tmp, mtmp, t) → res
l14(x, y, res, tmp, mtmp, t) → l15(x, y, res, tmp, monus(x, y), t)
l12(x, y, res, tmp, mtmp, t) → l13(x, y, res, tmp, monus(x, y), t)
l10(x, y, res, tmp, mtmp, t) → l11(x, y, res, tmp, mtmp, <(x, y))
gcd(x, y) → l1(x, y, 0, False, False, False)
equal0(a, b) → e1(a, b, False, False)
e8(a, b, res, t) → res
e3(a, b, res, t) → e4(a, b, res, <(b, a))
e1(a, b, res, t) → e2(a, b, res, <(a, b))
The (relative) TRS S consists of the following rules:
<(S(x), S(y)) → <(x, y)
<(0, S(y)) → True
<(x, 0) → False
Rewrite Strategy: INNERMOST
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
m4(S(x'), S(x), res, t) →+ m5(S(x'), S(x), m4(x', x, False, False), t)
gives rise to a decreasing loop by considering the right hand sides subterm at position [2].
The pumping substitution is [x' / S(x'), x / S(x)].
The result substitution is [res / False, t / False].
(2) BOUNDS(n^1, INF)